Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app'(app'(minus,x),0)  → x
2:    app'(app'(minus,app'(s,x)),app'(s,y))  → app'(app'(minus,x),y)
3:    app'(app'(quot,0),app'(s,y))  → 0
4:    app'(app'(quot,app'(s,x)),app'(s,y))  → app'(s,app'(app'(quot,app'(app'(minus,x),y)),app'(s,y)))
5:    app'(app'(le,0),y)  → true
6:    app'(app'(le,app'(s,x)),0)  → false
7:    app'(app'(le,app'(s,x)),app'(s,y))  → app'(app'(le,x),y)
8:    app'(app'(app,nil),y)  → y
9:    app'(app'(app,app'(app'(add,n),x)),y)  → app'(app'(add,n),app'(app'(app,x),y))
10:    app'(app'(low,n),nil)  → nil
11:    app'(app'(low,n),app'(app'(add,m),x))  → app'(app'(app'(if_low,app'(app'(le,m),n)),n),app'(app'(add,m),x))
12:    app'(app'(app'(if_low,true),n),app'(app'(add,m),x))  → app'(app'(add,m),app'(app'(low,n),x))
13:    app'(app'(app'(if_low,false),n),app'(app'(add,m),x))  → app'(app'(low,n),x)
14:    app'(app'(high,n),nil)  → nil
15:    app'(app'(high,n),app'(app'(add,m),x))  → app'(app'(app'(if_high,app'(app'(le,m),n)),n),app'(app'(add,m),x))
16:    app'(app'(app'(if_high,true),n),app'(app'(add,m),x))  → app'(app'(high,n),x)
17:    app'(app'(app'(if_high,false),n),app'(app'(add,m),x))  → app'(app'(add,m),app'(app'(high,n),x))
18:    app'(quicksort,nil)  → nil
19:    app'(quicksort,app'(app'(add,n),x))  → app'(app'(app,app'(quicksort,app'(app'(low,n),x))),app'(app'(add,n),app'(quicksort,app'(app'(high,n),x))))
There are 41 dependency pairs:
20:    APP'(app'(minus,app'(s,x)),app'(s,y))  → APP'(app'(minus,x),y)
21:    APP'(app'(minus,app'(s,x)),app'(s,y))  → APP'(minus,x)
22:    APP'(app'(quot,app'(s,x)),app'(s,y))  → APP'(s,app'(app'(quot,app'(app'(minus,x),y)),app'(s,y)))
23:    APP'(app'(quot,app'(s,x)),app'(s,y))  → APP'(app'(quot,app'(app'(minus,x),y)),app'(s,y))
24:    APP'(app'(quot,app'(s,x)),app'(s,y))  → APP'(quot,app'(app'(minus,x),y))
25:    APP'(app'(quot,app'(s,x)),app'(s,y))  → APP'(app'(minus,x),y)
26:    APP'(app'(quot,app'(s,x)),app'(s,y))  → APP'(minus,x)
27:    APP'(app'(le,app'(s,x)),app'(s,y))  → APP'(app'(le,x),y)
28:    APP'(app'(le,app'(s,x)),app'(s,y))  → APP'(le,x)
29:    APP'(app'(app,app'(app'(add,n),x)),y)  → APP'(app'(add,n),app'(app'(app,x),y))
30:    APP'(app'(app,app'(app'(add,n),x)),y)  → APP'(app'(app,x),y)
31:    APP'(app'(app,app'(app'(add,n),x)),y)  → APP'(app,x)
32:    APP'(app'(low,n),app'(app'(add,m),x))  → APP'(app'(app'(if_low,app'(app'(le,m),n)),n),app'(app'(add,m),x))
33:    APP'(app'(low,n),app'(app'(add,m),x))  → APP'(app'(if_low,app'(app'(le,m),n)),n)
34:    APP'(app'(low,n),app'(app'(add,m),x))  → APP'(if_low,app'(app'(le,m),n))
35:    APP'(app'(low,n),app'(app'(add,m),x))  → APP'(app'(le,m),n)
36:    APP'(app'(low,n),app'(app'(add,m),x))  → APP'(le,m)
37:    APP'(app'(app'(if_low,true),n),app'(app'(add,m),x))  → APP'(app'(add,m),app'(app'(low,n),x))
38:    APP'(app'(app'(if_low,true),n),app'(app'(add,m),x))  → APP'(app'(low,n),x)
39:    APP'(app'(app'(if_low,true),n),app'(app'(add,m),x))  → APP'(low,n)
40:    APP'(app'(app'(if_low,false),n),app'(app'(add,m),x))  → APP'(app'(low,n),x)
41:    APP'(app'(app'(if_low,false),n),app'(app'(add,m),x))  → APP'(low,n)
42:    APP'(app'(high,n),app'(app'(add,m),x))  → APP'(app'(app'(if_high,app'(app'(le,m),n)),n),app'(app'(add,m),x))
43:    APP'(app'(high,n),app'(app'(add,m),x))  → APP'(app'(if_high,app'(app'(le,m),n)),n)
44:    APP'(app'(high,n),app'(app'(add,m),x))  → APP'(if_high,app'(app'(le,m),n))
45:    APP'(app'(high,n),app'(app'(add,m),x))  → APP'(app'(le,m),n)
46:    APP'(app'(high,n),app'(app'(add,m),x))  → APP'(le,m)
47:    APP'(app'(app'(if_high,true),n),app'(app'(add,m),x))  → APP'(app'(high,n),x)
48:    APP'(app'(app'(if_high,true),n),app'(app'(add,m),x))  → APP'(high,n)
49:    APP'(app'(app'(if_high,false),n),app'(app'(add,m),x))  → APP'(app'(add,m),app'(app'(high,n),x))
50:    APP'(app'(app'(if_high,false),n),app'(app'(add,m),x))  → APP'(app'(high,n),x)
51:    APP'(app'(app'(if_high,false),n),app'(app'(add,m),x))  → APP'(high,n)
52:    APP'(quicksort,app'(app'(add,n),x))  → APP'(app'(app,app'(quicksort,app'(app'(low,n),x))),app'(app'(add,n),app'(quicksort,app'(app'(high,n),x))))
53:    APP'(quicksort,app'(app'(add,n),x))  → APP'(app,app'(quicksort,app'(app'(low,n),x)))
54:    APP'(quicksort,app'(app'(add,n),x))  → APP'(quicksort,app'(app'(low,n),x))
55:    APP'(quicksort,app'(app'(add,n),x))  → APP'(app'(low,n),x)
56:    APP'(quicksort,app'(app'(add,n),x))  → APP'(low,n)
57:    APP'(quicksort,app'(app'(add,n),x))  → APP'(app'(add,n),app'(quicksort,app'(app'(high,n),x)))
58:    APP'(quicksort,app'(app'(add,n),x))  → APP'(quicksort,app'(app'(high,n),x))
59:    APP'(quicksort,app'(app'(add,n),x))  → APP'(app'(high,n),x)
60:    APP'(quicksort,app'(app'(add,n),x))  → APP'(high,n)
The approximated dependency graph contains one SCC: {20,23,25,27,30,32,33,35,38,40,42,43,45,47,50,52,54,55,58,59}.
Tyrolean Termination Tool  (22.70 seconds)   ---  May 3, 2006